Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar16/CimeSLASHlse.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Case₃(m, xi, n), s) -> SUM_SUB₂(xi, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Case₃(m, xi, n), s) -> SUM_SUB₂(xi, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
SUM_SUB₂(x1, x2) = SUM_SUB₂(x1, x2)
Cons_sum₃(x1, x2, x3) = Cons_sum₁(x3)
Cons_usual₃(x1, x2, x3) = Cons_usual₃(x1, x2, x3)

Lexicographic Path Order [19].
Precedence:

Cons_usual₃ > [SUM_SUB₂, Cons_{sum_1]}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
TERM_SUB₂(x1, x2) = TERM_SUB₁(x2)
Term_var₁(x1) = x1
Cons_usual₃(x1, x2, x3) = Cons_usual₂(x2, x3)
Cons_sum₃(x1, x2, x3) = Cons_sum₃(x1, x2, x3)

Lexicographic Path Order [19].
Precedence:

Cons_sum₃ > [TERM_SUB₁, Cons_{usual_2]}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.